00005 00010 PRE_PRED: P,G; VAR:x,y,z; 00020 00100 ∀(x,y)(P(x,y) ∧P(y,z) ⊃ G(x,z)); 00300 ∀(y)∃(x)P(x,y); 00500 THM:∃(x,y)G(x,y); 00600 ;